YES 0.763 H-Termination proof of /home/matraf/haskell/eval_FullyBlown_Fast/Monad.hs
H-Termination of the given Haskell-Program with start terms could successfully be proven:



HASKELL
  ↳ LR

mainModule Monad
  ((liftM5 :: (b  ->  d  ->  e  ->  c  ->  f  ->  a ->  [b ->  [d ->  [e ->  [c ->  [f ->  [a]) :: (b  ->  d  ->  e  ->  c  ->  f  ->  a ->  [b ->  [d ->  [e ->  [c ->  [f ->  [a])

module Monad where
  import qualified Maybe
import qualified Prelude

  liftM5 :: Monad d => (g  ->  b  ->  c  ->  a  ->  e  ->  f ->  d g  ->  d b  ->  d c  ->  d a  ->  d e  ->  d f
liftM5 f m1 m2 m3 m4 m5 m1 >>= (\x1 ->m2 >>= (\x2 ->m3 >>= (\x3 ->m4 >>= (\x4 ->m5 >>= (\x5 ->return (f x1 x2 x3 x4 x5))))))


module Maybe where
  import qualified Monad
import qualified Prelude



Lambda Reductions:
The following Lambda expression
\x5return (f x1 x2 x3 x4 x5)

is transformed to
liftM50 f x1 x2 x3 x4 x5 = return (f x1 x2 x3 x4 x5)

The following Lambda expression
\x4m5 >>= liftM50 f x1 x2 x3 x4

is transformed to
liftM51 m5 f x1 x2 x3 x4 = m5 >>= liftM50 f x1 x2 x3 x4

The following Lambda expression
\x3m4 >>= liftM51 m5 f x1 x2 x3

is transformed to
liftM52 m4 m5 f x1 x2 x3 = m4 >>= liftM51 m5 f x1 x2 x3

The following Lambda expression
\x2m3 >>= liftM52 m4 m5 f x1 x2

is transformed to
liftM53 m3 m4 m5 f x1 x2 = m3 >>= liftM52 m4 m5 f x1 x2

The following Lambda expression
\x1m2 >>= liftM53 m3 m4 m5 f x1

is transformed to
liftM54 m2 m3 m4 m5 f x1 = m2 >>= liftM53 m3 m4 m5 f x1



↳ HASKELL
  ↳ LR
HASKELL
      ↳ BR

mainModule Monad
  ((liftM5 :: (d  ->  f  ->  c  ->  a  ->  b  ->  e ->  [d ->  [f ->  [c ->  [a ->  [b ->  [e]) :: (d  ->  f  ->  c  ->  a  ->  b  ->  e ->  [d ->  [f ->  [c ->  [a ->  [b ->  [e])

module Maybe where
  import qualified Monad
import qualified Prelude


module Monad where
  import qualified Maybe
import qualified Prelude

  liftM5 :: Monad f => (e  ->  b  ->  c  ->  g  ->  d  ->  a ->  f e  ->  f b  ->  f c  ->  f g  ->  f d  ->  f a
liftM5 f m1 m2 m3 m4 m5 m1 >>= liftM54 m2 m3 m4 m5 f

  
liftM50 f x1 x2 x3 x4 x5 return (f x1 x2 x3 x4 x5)

  
liftM51 m5 f x1 x2 x3 x4 m5 >>= liftM50 f x1 x2 x3 x4

  
liftM52 m4 m5 f x1 x2 x3 m4 >>= liftM51 m5 f x1 x2 x3

  
liftM53 m3 m4 m5 f x1 x2 m3 >>= liftM52 m4 m5 f x1 x2

  
liftM54 m2 m3 m4 m5 f x1 m2 >>= liftM53 m3 m4 m5 f x1



Replaced joker patterns by fresh variables and removed binding patterns.

↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
HASKELL
          ↳ COR

mainModule Monad
  ((liftM5 :: (b  ->  d  ->  c  ->  e  ->  a  ->  f ->  [b ->  [d ->  [c ->  [e ->  [a ->  [f]) :: (b  ->  d  ->  c  ->  e  ->  a  ->  f ->  [b ->  [d ->  [c ->  [e ->  [a ->  [f])

module Monad where
  import qualified Maybe
import qualified Prelude

  liftM5 :: Monad a => (g  ->  e  ->  c  ->  d  ->  f  ->  b ->  a g  ->  a e  ->  a c  ->  a d  ->  a f  ->  a b
liftM5 f m1 m2 m3 m4 m5 m1 >>= liftM54 m2 m3 m4 m5 f

  
liftM50 f x1 x2 x3 x4 x5 return (f x1 x2 x3 x4 x5)

  
liftM51 m5 f x1 x2 x3 x4 m5 >>= liftM50 f x1 x2 x3 x4

  
liftM52 m4 m5 f x1 x2 x3 m4 >>= liftM51 m5 f x1 x2 x3

  
liftM53 m3 m4 m5 f x1 x2 m3 >>= liftM52 m4 m5 f x1 x2

  
liftM54 m2 m3 m4 m5 f x1 m2 >>= liftM53 m3 m4 m5 f x1


module Maybe where
  import qualified Monad
import qualified Prelude



Cond Reductions:
The following Function with conditions
undefined 
 | False
 = undefined

is transformed to
undefined  = undefined1

undefined0 True = undefined

undefined1  = undefined0 False



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
HASKELL
              ↳ Narrow

mainModule Monad
  (liftM5 :: (c  ->  f  ->  b  ->  d  ->  a  ->  e ->  [c ->  [f ->  [b ->  [d ->  [a ->  [e])

module Maybe where
  import qualified Monad
import qualified Prelude


module Monad where
  import qualified Maybe
import qualified Prelude

  liftM5 :: Monad b => (f  ->  d  ->  g  ->  c  ->  a  ->  e ->  b f  ->  b d  ->  b g  ->  b c  ->  b a  ->  b e
liftM5 f m1 m2 m3 m4 m5 m1 >>= liftM54 m2 m3 m4 m5 f

  
liftM50 f x1 x2 x3 x4 x5 return (f x1 x2 x3 x4 x5)

  
liftM51 m5 f x1 x2 x3 x4 m5 >>= liftM50 f x1 x2 x3 x4

  
liftM52 m4 m5 f x1 x2 x3 m4 >>= liftM51 m5 f x1 x2 x3

  
liftM53 m3 m4 m5 f x1 x2 m3 >>= liftM52 m4 m5 f x1 x2

  
liftM54 m2 m3 m4 m5 f x1 m2 >>= liftM53 m3 m4 m5 f x1



Haskell To QDPs


↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_psPs(:(vy100, vy101), vy9, h) → new_psPs(vy101, vy9, h)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs(:(vy80, vy81), vy3, vy40, vy50, vy60, vy70, h, ba, bb, bc, bd, be) → new_gtGtEs(vy81, vy3, vy40, vy50, vy60, vy70, h, ba, bb, bc, bd, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs0(:(vy70, vy71), vy8, vy3, vy40, vy50, vy60, h, ba, bb, bc, bd, be) → new_gtGtEs0(vy71, vy8, vy3, vy40, vy50, vy60, h, ba, bb, bc, bd, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs1(:(vy60, vy61), vy7, vy8, vy3, vy40, vy50, h, ba, bb, bc, bd, be) → new_gtGtEs1(vy61, vy7, vy8, vy3, vy40, vy50, h, ba, bb, bc, bd, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof
                  ↳ QDP

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs2(:(vy50, vy51), vy6, vy7, vy8, vy3, vy40, h, ba, bb, bc, bd, be) → new_gtGtEs2(vy51, vy6, vy7, vy8, vy3, vy40, h, ba, bb, bc, bd, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs:



↳ HASKELL
  ↳ LR
    ↳ HASKELL
      ↳ BR
        ↳ HASKELL
          ↳ COR
            ↳ HASKELL
              ↳ Narrow
                ↳ AND
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
                  ↳ QDP
QDP
                    ↳ QDPSizeChangeProof

Q DP problem:
The TRS P consists of the following rules:

new_gtGtEs3(:(vy40, vy41), vy5, vy6, vy7, vy8, vy3, h, ba, bb, bc, bd, be) → new_gtGtEs3(vy41, vy5, vy6, vy7, vy8, vy3, h, ba, bb, bc, bd, be)

R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
By using the subterm criterion [20] together with the size-change analysis [32] we have proven that there are no infinite chains for this DP problem.

From the DPs we obtained the following set of size-change graphs: